DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2023.15

Closure Properties of General Grammars – Formally Verified

Authors: Martin Dvorak and Jasmin Blanchette

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract

We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.

Cite as

Martin Dvorak and Jasmin Blanchette. Closure Properties of General Grammars – Formally Verified. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15,
  author =	{Dvorak, Martin and Blanchette, Jasmin},
  title =	{{Closure Properties of General Grammars – Formally Verified}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
  URN =		{urn:nbn:de:0030-drops-183906},
  doi =		{10.4230/LIPIcs.ITP.2023.15},
  annote =	{Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}
}

Document

DOI: 10.4230/LIPIcs.ITP.2022.8

Seventeen Provers Under the Hammer

Authors: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract

One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.

Cite as

Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
  author =	{Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
  title =	{{Seventeen Provers Under the Hammer}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
  URN =		{urn:nbn:de:0030-drops-167178},
  doi =		{10.4230/LIPIcs.ITP.2022.8},
  annote =	{Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}

Search Results

Documents authored by Blanchette, Jasmin

Closure Properties of General Grammars – Formally Verified

Abstract

Cite as

Seventeen Provers Under the Hammer

Abstract

Cite as

Thanks for your feedback!

Could not send message